Nuprl Lemma : maximal-in-list
11,40
postcript
pdf
A
:Type,
f
:(
A
),
L
:(
A
List). (0 < ||
L
||)
(
a
L
.
x
L
. (
f
(
x
))
(
f
(
a
)))
latex
Definitions
(
x
L
.
P
(
x
))
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
t
T
,
,
x
.
t
(
x
)
,
P
Q
,
A
B
,
A
,
False
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
P
Q
,
P
Q
Lemmas
l
member
wf
,
l
all
wf2
,
le
wf
,
member
singleton
,
l
all
cons
,
l
all
nil
origin
A:Type, f:(A
), L:(A List). (0 < ||L||) 
(
a
L.xL. (f(x)) 
(f(a))) A:Type, f:(A), L:(A List). (0 < ||L||) (aL.xL. (f(x)) (f(a))) xL.P(x))x:A. B(x) T
x. t(x) Q B
Ax:A. B(x)
Q Q